Theorem vtoclbg 3523

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 3520	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  3617  pm13.183  3632  elab6g  3635  elabgw  3644  sbc8g  3761  sbc2or  3762  sbccow  3776  sbcco  3779  sbc5ALT  3782  sbcie2g  3794  eqsbc1  3800  sbcng  3801  sbcimg  3802  sbcan  3803  sbcor  3804  sbcbig  3805  sbcal  3813  sbcex2  3814  sbcel1v  3819  sbcreu  3839  csbiebg  3894  sbcel12  4374  sbceqg  4375  csbie2df  4406  preq12bg  4817  elintrabg  4925  sbcbr123  5161  inisegn0  6069  fsn2g  7110  funfvima3  7210  elixpsn  8910  ixpsnf1o  8911  domeng  8934  1sdomOLD  9196  rankcf  10730  eldm3  35748  elima4  35763  brsset  35877  brbigcup  35886  elfix2  35892  elfunsg  35904  elsingles  35906  funpartlem  35930  ellines  36140  elhf2g  36164  bj-elpwgALT  37042  cover2g  37710  sbcrexgOLD  42773