Theorem rcla4cva 1879

Description: Restricted specialization with implicit substitution.

Hypothesis

Ref	Expression
rcla4v.1	⊢ (x = A → (φ ↔ ψ))

Assertion

Ref	Expression
rcla4cva	⊢ ((∀x ∈ B φ ⋀ A ∈ B) → ψ)

Distinct variable groups:   x,A   x,B   ψ,x

Proof of Theorem rcla4cva

Step	Hyp	Ref	Expression
1		rcla4v.1	. . 3 ⊢ (x = A → (φ ↔ ψ))
2	1	rcla4va 1878	. 2 ⊢ ((A ∈ B ⋀ ∀x ∈ B φ) → ψ)
3	2	ancoms 438	1 ⊢ ((∀x ∈ B φ ⋀ A ∈ B) → ψ)

Syntax hints:   → wi 3   ↔ wb 146   ⋀ wa 223   = wceq 958   ∈ wcel 960  ∀wral 1648

This theorem is referenced by:  disjne 2319  fconstfv 3855  odi 4216  omsmolem 4262  unblem1 4551  supmo 4585  sqr2irrlem3 6727  cau3ir 6915  climrecl 7110  climge0 7112  climcau 7156  infxpidmlem10 7562  elcls3 7708  iscncl 7767  metcnp 7884  cmscvg 7944  grpidinvlem3 8047  grpidinv 8049  grpidinv2 8056  vcid 8166  lnopeq0 9927  csmdsym 10256

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-ral 1652  df-v 1815

Copyright terms: Public domain