Theorem vtoclbg 3520

Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 29-Apr-1994.)

Hypotheses

Ref	Expression
vtoclbg.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))
vtoclbg.2	⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃))
vtoclbg.3	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
vtoclbg	⊢ (𝐴 ∈ 𝑉 → (𝜒 ↔ 𝜃))

Distinct variable groups:   𝑥,𝐴   𝜒,𝑥   𝜃,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)   𝑉(𝑥)

Proof of Theorem vtoclbg

Step	Hyp	Ref	Expression
1		vtoclbg.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))
2		vtoclbg.2	. . 3 ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃))
3	1, 2	bibi12d 345	. 2 ⊢ (𝑥 = 𝐴 → ((𝜑 ↔ 𝜓) ↔ (𝜒 ↔ 𝜃)))
4		vtoclbg.3	. 2 ⊢ (𝜑 ↔ 𝜓)
5	3, 4	vtoclg 3517	1 ⊢ (𝐴 ∈ 𝑉 → (𝜒 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-clel 2803

This theorem is referenced by:  alexeqg  3614  pm13.183  3629  elab6g  3632  elabgw  3641  sbc8g  3758  sbc2or  3759  sbccow  3773  sbcco  3776  sbc5ALT  3779  sbcie2g  3791  eqsbc1  3797  sbcng  3798  sbcimg  3799  sbcan  3800  sbcor  3801  sbcbig  3802  sbcal  3810  sbcex2  3811  sbcel1v  3816  sbcreu  3836  csbiebg  3891  sbcel12  4370  sbceqg  4371  csbie2df  4402  preq12bg  4813  elintrabg  4921  sbcbr123  5156  inisegn0  6058  fsn2g  7092  funfvima3  7192  elixpsn  8887  ixpsnf1o  8888  domeng  8911  1sdomOLD  9172  rankcf  10706  eldm3  35721  elima4  35736  brsset  35850  brbigcup  35859  elfix2  35865  elfunsg  35877  elsingles  35879  funpartlem  35903  ellines  36113  elhf2g  36137  bj-elpwgALT  37015  cover2g  37683  sbcrexgOLD  42746